COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002								    NIC 24934
C00015 ENDMK
C⊗;
							    NIC 24934
						    Part of NIC 24980

	    STANFORD ARTIFICIAL INTELLIGENCE LABORATORY
		    1974 ARPA Project Summary

Prepared for:	ARPA IPTO Principal Investigators Meeting
		March 12-14, 1975

Prepared by:	John McCarthy
		Computer Science Department
		Stanford University
		Stanford, California 94305

FORMAL REASONING - John McCarthy, Richard Weyhrauch, et al

Using our  LCF proof-checker, we  have produced an  axiomatization of
the programming language PASCAL.  This represents a major step toward
using LCF as a practical program verification system. 

AUTOMATIC DEDUCTION - David Luckham, et al

A successful new automatic programming system accepts descriptions of
library routines,  programming methods, and program specifications in
a high  level  semantic definition  language.   It  returns  programs
written  in a subset of  ALGOL that satisfy the given specifications. 
Experimental  applications  include computing  arithmetical functions
and planning robot strategies. 

Another system  works  with algorithms  expressed  in a  higher-level
language  and automatically chooses  an efficient  representation for
the data  structure.   It  then produces  a  program that  uses  this
representation.  Representations considered include  certain kinds of
linked-lists, binary trees, and hash tables. 

PROGRAM UNDERSTANDING SYSTEMS - Cordell Green, et al

The EXAMPLE program  that infers recursive  list-processing functions
from  example input-output  pairs was  completed  during 1974.   This
system demonstrates the possibility  of using fairly natural  methods
of program specification. 

The  PUP  system  was  our  first  to  show  a  rudimentary  "program
understanding"  behavior.  By following a  simple chain of reasoning,
it can  synthesize  a  few short  programs,  such as  interchange  of
elements, three-element sort, and integer square root. 

A system was  completed which, given a program  expressed in terms of
high-level information  structures such  as sets,  ordered sets,  and
relations,  automatically   chooses  efficient   implementation-level
representations  and produces an  equivalent program  that uses these
representations. 

A very comprehensive dialog was completed which exhibits  a knowledge
base of  rules for the  synthesis of sorting programs.   Although not
all  the   necessary  synthesis  rules  have  been  codified,  it  is
reasonably clear how  to do so.   This work  is aimed at the  deepest
understanding of a simple program synthesis yet attempted. 

Work was  completed on a pilot system  that interactively synthesizes
what is essentially Winston's concept formation program.  This system
points  toward   the  feasibility  of   systems  for   writing  long,
domain-specific programs. 

NATURAL LANGUAGE UNDERSTANDING

A system called MARGIE was completed that links natural language
understanding, inference, and generation of natural language output.
This is the first such system with a strong theoretical basis, namely
Conceptual Dependency.

HAND-EYE RESEARCH

We have developed a two-arm  synchronized manipulation capability and
tested  it on several mechanical  assembly tasks that  are beyond the
capability of a single arm.  A new high-level "hand  language" called
HAL has been developed for specifying advanced manipulation tasks. 

We have used near and far field stereo  vision and motion parallax to
locate  objects spatially and to automatically generate contour maps. 
Another program can recognize things of the complexity of a doll or a
hammer in various positions, using a laser triangulation system. 

TRAINING

During  the   year,  six  members   of  our  staff   published  Ph.D.
dissertations  and  another  32  graduate  students  received  direct
support.